$Q$ $\leftarrow\leftarrow$= $f$== $P$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$Q$ $\leftarrow$==$f$== $P$ \& ($\forall$$e$:\{$e$:E$\mid$ $Q$($e$)\} . $\exists$${\it e'}$:\{$e$:E$\mid$ $P$($e$)\} . ($f$(${\it e'}$) = $e$))